\begin{tabbing}
$\forall$$M_{1}$, $M_{2}$:MsgA.
\\[0ex]$M_{1}$ $\subseteq$ $M_{2}$
\\[0ex]$\Rightarrow$ (\=$\forall$$k$:Knd, $x$:Id, $s$:$M_{2}$.state, $v$:$M_{2}$.da($k$), $w$:$M_{2}$.ds($x$).\+
\\[0ex]$M_{2}$.ef($k$,$x$,$s$,$v$,$w$) $\Rightarrow$ $M_{1}$.ef($k$,$x$,$s$,$v$,$w$))
\-
\end{tabbing}